(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 6))
(declare-fun a1 () (Array  (_ BitVec 13)  (_ BitVec 5)))
(assert (let ((e2(_ bv38141 16)))
(let ((e3 (ite (bvuge ((_ sign_extend 10) v0) e2) (_ bv1 1) (_ bv0 1))))
(let ((e4 (store a1 ((_ sign_extend 12) e3) ((_ sign_extend 4) e3))))
(let ((e5 (store a1 ((_ extract 15 3) e2) ((_ extract 4 0) v0))))
(let ((e6 (select e5 ((_ extract 14 2) e2))))
(let ((e7 (select e4 ((_ zero_extend 7) v0))))
(let ((e8 (store a1 ((_ sign_extend 7) v0) e6)))
(let ((e9 (select e5 ((_ sign_extend 7) v0))))
(let ((e10 (store e5 ((_ extract 15 3) e2) ((_ extract 4 0) v0))))
(let ((e11 (select e8 ((_ sign_extend 8) e9))))
(let ((e12 (bvmul v0 ((_ zero_extend 1) e7))))
(let ((e13 (concat e9 e7)))
(let ((e14 (ite (bvult e6 e9) (_ bv1 1) (_ bv0 1))))
(let ((e15 (bvnor e11 e6)))
(let ((e16 ((_ zero_extend 7) e3)))
(let ((e17 (bvcomp e2 ((_ sign_extend 11) e6))))
(let ((e18 (= e9 ((_ zero_extend 4) e17))))
(let ((e19 (bvslt v0 ((_ sign_extend 5) e17))))
(let ((e20 (bvsgt v0 ((_ sign_extend 1) e6))))
(let ((e21 (bvsge v0 ((_ zero_extend 1) e11))))
(let ((e22 (bvule e7 e7)))
(let ((e23 (bvult e16 e16)))
(let ((e24 (bvslt e16 ((_ sign_extend 3) e6))))
(let ((e25 (distinct ((_ sign_extend 9) e17) e13)))
(let ((e26 (bvuge e2 ((_ zero_extend 15) e14))))
(let ((e27 (bvugt e14 e17)))
(let ((e28 (bvugt e16 ((_ zero_extend 7) e17))))
(let ((e29 (bvsle ((_ zero_extend 5) e3) e12)))
(let ((e30 (bvule ((_ sign_extend 9) e14) e13)))
(let ((e31 (bvule e13 ((_ sign_extend 5) e15))))
(let ((e32 (not e18)))
(let ((e33 (not e31)))
(let ((e34 (and e22 e26)))
(let ((e35 (= e34 e30)))
(let ((e36 (not e29)))
(let ((e37 (= e21 e25)))
(let ((e38 (xor e32 e24)))
(let ((e39 (= e19 e38)))
(let ((e40 (and e37 e20)))
(let ((e41 (= e33 e27)))
(let ((e42 (and e41 e36)))
(let ((e43 (xor e42 e40)))
(let ((e44 (and e43 e43)))
(let ((e45 (ite e44 e23 e23)))
(let ((e46 (or e39 e28)))
(let ((e47 (ite e45 e45 e45)))
(let ((e48 (= e46 e46)))
(let ((e49 (xor e48 e35)))
(let ((e50 (and e47 e49)))
e50
))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
